$\forall$$T$:Type, ${\it as}$, ${\it bs}$, ${\it cs}$, ${\it ds}$:$T$ List.
\\[0ex](${\it as}$ @ ${\it cs}$) $=$ (${\it bs}$ @ ${\it ds}$) $\in$ $T$ List
\\[0ex]$\Rightarrow$ $\parallel$${\it as}$$\parallel$ $=$ $\parallel$${\it bs}$$\parallel$ $\in$ $\mathbb{Z}$ $\vee$ $\parallel$${\it cs}$$\parallel$ $=$ $\parallel$${\it ds}$$\parallel$ $\in$ $\mathbb{Z}$
\\[0ex]$\Rightarrow$ \{${\it as}$ $=$ ${\it bs}$ \& ${\it cs}$ $=$ ${\it ds}$\}